Built with Alectryon, running Coq+SerAPI v8.13.0+0.13.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
From hanoi Require Import extra.Set Implicit Arguments.Unset Strict Implicit.Unset Printing Implicit Defensive.SectionMain.Variableab : nat.HypothesisaL1 : 1 < a.HypothesisaLb : a < b.HypothesisaCb : coprime a b.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
1 < b
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
1 < b
byapply: ltn_trans aLb.Qed.Fixpointalphal (n : nat) :=
if n isn't n1.+1then [:: 1; a; b]
elseletl := alphal n1 in
merge leq
(letc := head 1 l inletl1 := if b * c \in l then [::] else [:: b * c] inif a * c \in l then l1 else a * c :: l1)
(behead l).Definitionalphan := head 1 (alphal n).
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
T:eqType
r:rel T
l:seq T
sorted r l -> sorted r (behead l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
T:eqType
r:rel T
l:seq T
sorted r l -> sorted r (behead l)
bycase: l => //= a1 [|b1 l /andP[]].Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
sorted leq (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
sorted leq (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:sorted leq (alphal n)
sorted leq
(merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:sorted leq (alphal n)
sorted leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:sorted leq (alphal n)
sorted leq (behead (alphal n))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:sorted leq (alphal n)
sorted leq (behead (alphal n))
byapply: behead_sorted.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
i \in [:: 1; a; b] -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(foralli : nat, i \in alphal n -> 0 < i) ->
foralli : nat,
i
\in merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)) -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(foralli : nat, i \in alphal n -> 0 < i) ->
foralli : nat,
i
\in merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)) -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
(i == a * 1) || (i == b * 1) -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
i
\in merge leq
(if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) l -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
i
\in merge leq
(if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) l -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
H1:0 < a1
i
\in merge leq
(if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) l -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
H1:0 < a1
i1:nat_eqType
i1 \in l -> 0 < i1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
H1:0 < a1
IH1:foralli1 : nat_eqType, i1 \in l -> 0 < i1
i
\in merge leq
(if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) l -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
H1:0 < a1
IH1:foralli1 : nat_eqType, i1 \in l -> 0 < i1
i
\in merge leq
(if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) l -> 0 < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, a1:nat
l:seq nat
IH:foralli : nat, i \in a1 :: l -> 0 < i
i:nat
H1:0 < a1
IH1:foralli1 : nat_eqType, i1 \in l -> 0 < i1
i
\in (if (a * a1 == a1) || (a * a1 \in l)
thenif (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1]
else
a * a1
:: (if (b * a1 == a1) || (b * a1 \in l)
then [::]
else [:: b * a1])) ++ l -> 0 < i
merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)) != [::]
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
size
((if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n)) != 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
H:foralli : nat, i \in c :: l -> 0 < i
size
((if a * c \in c :: l
thenif b * c \in c :: l then [::] else [:: b * c]
else
a * c
:: (if b * c \in c :: l then [::] else [:: b * c])) ++
l) != 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
H:foralli : nat, i \in c :: l -> 0 < i
E:(a * c \in c :: l) = true
size ([::] ++ l) != 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
0 < c ->
(a * c == c) = true ->
1 < a -> size ([::] ++ [::]) != 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c1:nat
(a * c1.+1 == c1.+1) = true ->
1 < a -> size ([::] ++ [::]) != 0
uniq
(merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:uniq (alphal n)
uniq
(merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(a * 1 \notin [:: b * 1]) && true
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
uniq
(merge leq
(if a * c \in c :: l
thenif b * c \in c :: l then [::] else [:: b * c]
else
a * c
:: (if b * c \in c :: l
then [::]
else [:: b * c])) l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
uniq
(merge leq
(if a * c \in c :: l
thenif b * c \in c :: l then [::] else [:: b * c]
else
a * c
:: (if b * c \in c :: l
then [::]
else [:: b * c])) l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \in c :: l
H2:b * c \notin c :: l
b * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \in c :: l
a * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \notin c :: l
(a * c \notin b * c :: l) && (b * c \notin l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \in c :: l
H2:b * c \notin c :: l
b * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \in c :: l
a * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \notin c :: l
(a * c \notin b * c :: l) && (b * c \notin l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \in c :: l
a * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \notin c :: l
(a * c \notin b * c :: l) && (b * c \notin l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \in c :: l
a * c \notin l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \notin c :: l
(a * c \notin b * c :: l) && (b * c \notin l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
H1:a * c \notin c :: l
H2:b * c \notin c :: l
(a * c \notin b * c :: l) && (b * c \notin l)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
U:foralli : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
(a * c != b * c) && true && true
byrewrite eqn_mul2r negb_or !neq_ltn aLb U ?orbT // inE eqxx.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
alpha n < alpha n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
alpha n < alpha n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
head 1 (alphal n) <
head 1
(merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
h <
head 1
(merge leq
(if a * h \in alphal n
thenif b * h \in alphal n then [::] else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
0 < h
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
h <
head 1
(merge leq
(if a * h \in alphal n
thenif b * h \in alphal n then [::] else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
0 < head 1 (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
h <
head 1
(merge leq
(if a * h \in alphal n
thenif b * h \in alphal n then [::] else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
c:nat
l:seq nat
c \in c :: l
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
h <
head 1
(merge leq
(if a * h \in alphal n
thenif b * h \in alphal n then [::] else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
h <
head 1
(merge leq
(if a * h \in alphal n
thenif b * h \in alphal n then [::] else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
h < head 1 l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
head 1 l1 \in l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
h < head 1 l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)) != [::] -> head 1 l1 \in l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
h < head 1 l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
h < head 1 l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
hLi:foralli : nat_eqType, i \in l1 -> h < i
h < head 1 l1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
i \in l1 -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
i \in l1 -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
(i
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])))
|| (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
(i
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])))
|| (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \in alphal n
H2:b * h \notin alphal n
(i == b * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \in alphal n
(i == a * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \notin alphal n
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) ->
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \in alphal n
H2:b * h \notin alphal n
(i == b * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \in alphal n
(i == a * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \notin alphal n
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) ->
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \in alphal n
(i == a * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \notin alphal n
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) ->
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \in alphal n
(i == a * h) || (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \notin alphal n
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) ->
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
hLi1:i \in behead (alphal n) -> h < i
H1:a * h \notin alphal n
H2:b * h \notin alphal n
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) -> h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
subseq [:: h; i] (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
subseq [:: h; i] (h :: behead (alphal n))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
alphal n = h :: behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
subseq [:: i] (behead (alphal n))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
alphal n = h :: behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
alphal n = h :: behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h]))
(behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
h < i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
(h != i) && (h <= i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
(h <= i) && true -> (h != i) && (h <= i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
hIl1:head 1 l1 \in l1
i:nat_eqType
H:i \in behead (alphal n)
hsSa:subseq [:: h; i] (alphal n)
(h != i) && true
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
hP:0 < h
l1:=merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)):seq nat
bycase: n => // n; apply: leq_ltn_trans (alpha_ltn _).Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
n < alpha n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
n < alpha n
byelim: n => // n IH; apply: leq_trans (alpha_ltn _).Qed.DefinitionisABi := existsm, i = a ^ m.1 * b ^ m.2.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB (a ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB (a ^ i)
byexists (i, 0); rewrite muln1.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB (b ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB (b ^ i)
byexists (0, i); rewrite mul1n.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB i -> isAB (a * i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB i -> isAB (a * i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i, m1, m2:nat
a * (a ^ m1 * b ^ m2) =
a ^ (m1.+1, m2).1 * b ^ (m1.+1, m2).2
byrewrite !mulnA expnS.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB i -> isAB (b * i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB i -> isAB (b * i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i, m1, m2:nat
b * (a ^ m1 * b ^ m2) =
a ^ (m1, m2.+1).1 * b ^ (m1, m2.+1).2
byrewrite mulnCA expnS.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
[|| i == 1, i == a | i == b] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB a
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB b
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i:nat
isAB b
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
existsm : nat * nat,
head 1 (alphal n) = a ^ m.1 * b ^ m.2
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
c:nat
l:seq nat
F1:foralli : nat, i \in c :: l -> isAB i
existsm : nat * nat, c = a ^ m.1 * b ^ m.2
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i \in behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i \in behead (alphal n) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
b * head 1 (alphal n) =
a ^ (m1, m2.+1).1 * b ^ (m1, m2.+1).2
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
a * head 1 (alphal n) =
a ^ (m1.+1, m2).1 * b ^ (m1.+1, m2).2
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
[|| i == a * head 1 (alphal n),
i == b * head 1 (alphal n)
| i \in behead (alphal n)] -> isAB i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
isAB (a * head 1 (alphal n))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
isAB (b * head 1 (alphal n))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
IH:foralli : nat, i \in alphal n -> isAB i
i:nat
F:i \in behead (alphal n) ->
existsm : nat * nat, i = a ^ m.1 * b ^ m.2
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
i \in alphal n -> i != alpha n -> i \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n -> i != alpha n -> i \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
0 < alpha n ->
i \in alphal n -> i != alpha n -> i \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
0 < head 1 (alphal n) ->
i \in alphal n ->
i != head 1 (alphal n) ->
(i \in behead (alphal n))
|| (i
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])))
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
c:nat
l:seq nat
cP:0 < c
i \in c :: l ->
i != c ->
(i \in l)
|| (i
\in (if a * c \in c :: l
thenif b * c \in c :: l
then [::]
else [:: b * c]
else
a * c
:: (if b * c \in c :: l
then [::]
else [:: b * c])))
byrewrite inE => /orP[/eqP->|->//]; rewrite eqxx.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
alpha n \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
alpha n \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
alphal n != [::] -> alpha n \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, c:nat
l:seq nat
true -> c \in c :: l
byrewrite inE eqxx.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n.+1 ->
i != a * alpha n -> i != b * alpha n -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i \in alphal n.+1 ->
i != a * alpha n -> i != b * alpha n -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
i
\in merge leq
(if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]))
(behead (alphal n)) ->
i != a * head 1 (alphal n) ->
i != b * head 1 (alphal n) -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
h:=head 1 (alphal n):nat
i
\in merge leq
(if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) (behead (alphal n)) ->
i != a * h -> i != b * h -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
h:=head 1 (alphal n):nat
i \in behead (alphal n) ->
i != a * h -> i != b * h -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
h:=head 1 (alphal n):nat
i
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ->
i != a * h -> i != b * h -> i \in alphal n
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
i:nat_eqType
h:=head 1 (alphal n):nat
i
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ->
i != a * h -> i != b * h -> i \in alphal n
(a * alpha n \in alphal n ->
a * alpha n != alpha n -> a * alpha n \in alphal n.+1) ->
0 < alpha n -> a * alpha n \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(a * head 1 (alphal n) \in alphal n ->
a * head 1 (alphal n) != head 1 (alphal n) ->
a * head 1 (alphal n)
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n)) ->
0 < head 1 (alphal n) ->
a * head 1 (alphal n)
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
(a * h \in alphal n ->
a * h != h ->
a * h
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
H:a * h \in alphal n
H1:true ->
a * h != h ->
a * h
\in (if b * h \in alphal n
then [::]
else [:: b * h]) ++ behead (alphal n)
H2:0 < h
a * h
\in (if b * h \in alphal n then [::] else [:: b * h]) ++
behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
a * h \notin alphal n ->
(false ->
a * h != h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
H:a * h \in alphal n
H2:0 < h
a * h != h
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
a * h \notin alphal n ->
(false ->
a * h != h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
a * h \notin alphal n ->
(false ->
a * h != h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
\in (a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)
byrewrite mem_cat inE eqxx.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
b * alpha n \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
b * alpha n \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
0 < alpha n -> b * alpha n \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(b * alpha n \in alphal n ->
b * alpha n != alpha n -> b * alpha n \in alphal n.+1) ->
0 < alpha n -> b * alpha n \in alphal n.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
(b * head 1 (alphal n) \in alphal n ->
b * head 1 (alphal n) != head 1 (alphal n) ->
b * head 1 (alphal n)
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n)) ->
0 < head 1 (alphal n) ->
b * head 1 (alphal n)
\in (if a * head 1 (alphal n) \in alphal n
thenif b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)]
else
a * head 1 (alphal n)
:: (if b * head 1 (alphal n) \in alphal n
then [::]
else [:: b * head 1 (alphal n)])) ++
behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
(b * h \in alphal n ->
b * h != h ->
b * h
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
b * h
\in (if a * h \in alphal n
thenif b * h \in alphal n
then [::]
else [:: b * h]
else
a * h
:: (if b * h \in alphal n
then [::]
else [:: b * h])) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
H:b * h \in alphal n
H1:true ->
b * h != h ->
b * h
\in (if a * h \in alphal n
then [::]
else [:: a * h]) ++ behead (alphal n)
H2:0 < h
b * h
\in (if a * h \in alphal n then [::] else [:: a * h]) ++
behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
b * h \notin alphal n ->
(false ->
b * h != h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)) ->
0 < h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
H:b * h \in alphal n
H2:0 < h
b * h != h
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
b * h \notin alphal n ->
(false ->
b * h != h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)) ->
0 < h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n:nat
h:=head 1 (alphal n):nat
b * h \notin alphal n ->
(false ->
b * h != h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)) ->
0 < h ->
b * h
\in (if a * h \in alphal n
then [:: b * h]
else [:: a * h; b * h]) ++ behead (alphal n)
byrewrite -[X in X < _]mul1n ltn_mul2r alpha_gt0.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i, v:nat
isAB v -> v < alpha i.+1 -> v <= alpha i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i, v:nat
isAB v -> v < alpha i.+1 -> v <= alpha i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
i, v:nat
isAB:Main.isAB v
(alpha i < v -> alpha i.+1 <= v) ->
v < alpha i.+1 -> v <= alpha i
bydo2case: leqP => // _.Qed.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
i <= n ->
\sum_(j < n) alpha j <=
a * (\sum_(j < n - i) alpha j) + \sum_(j < i) b ^ j
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
i <= n ->
\sum_(j < n) alpha j <=
a * (\sum_(j < n - i) alpha j) + \sum_(j < i) b ^ j
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
\sum_(j < n) alpha j <=
a * (\sum_(j < n - i) alpha j) + \sum_(j < i) b ^ j
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
\sum_(0 <= i < n) alpha i <=
\sum_(0 <= i < n - i) a * alpha i +
\sum_(0 <= i < i) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
aux:foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i + \sum_(n1 <= i0 < n1 + w) b ^ i0
\sum_(0 <= i < n) alpha i <=
\sum_(0 <= i < n - i) a * alpha i +
\sum_(0 <= i < i) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
aux:foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i + \sum_(n1 <= i0 < n1 + w) b ^ i0
\sum_(0 <= i < 0 + n) alpha i <=
\sum_(0 <= i < 0 + (n - i)) a * alpha i +
\sum_(0 <= i < 0 + i) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
n = n - i + i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(n - i != 0) * alpha 0 <= a * alpha 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(i != 0) * alpha 0 <= b ^ 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
n = n - i + i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(n - i != 0) * alpha 0 <= a * alpha 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(i != 0) * alpha 0 <= b ^ 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(n - i != 0) * alpha 0 <= a * alpha 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(i != 0) * alpha 0 <= b ^ 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(n - i != 0) * alpha 0 <= a * alpha 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(i != 0) * alpha 0 <= b ^ 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
(i != 0) * alpha 0 <= b ^ 0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i:nat
iLn:i <= n
foralluvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i, j, k:nat
(0 != 0) * alpha i <= b ^ k ->
\sum_(i <= i0 < i + 0) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, i, j, k:nat
(0 != 0) * alpha i <= b ^ k ->
\sum_(i <= i0 < i + 0) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
(b ^ k + \sum_(k.+1 <= i < k + w.+1) b ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
b ^ k +
(\sum_(j <= i < j + 0) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k.+1 <= i < k.+1 + w) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
(w != 0) * alpha i.+1 <= b ^ k.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
w1:nat
(w1.+1 != 0) * alpha i.+1 <= b ^ k.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
w1:nat
aM2:alpha i <= b ^ k
alpha i.+1 <= b ^ k.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
w1:nat
aM2:alpha i <= b ^ k
a * alpha i <= b ^ k.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
w1:nat
aM2:alpha i <= b ^ k
alpha i.+1 <= a * alpha i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
w1:nat
aM2:alpha i <= b ^ k
alpha i.+1 <= a * alpha i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j + \sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j +
(\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j.+1 <= i < j.+1 + v) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
(v != 0) * alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
v1:nat
(v1.+1 != 0) * alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM2:(0 != 0) * alpha i <= b ^ k
v1:nat
aM1:alpha i <= a * alpha j
alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM2:(0 != 0) * alpha i <= b ^ k
v1:nat
aM1:alpha i <= a * alpha j
alpha i < a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM2:(0 != 0) * alpha i <= b ^ k
v1:nat
a * alpha j < a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM1:alpha i <= a * alpha j
alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM1:alpha i <= a * alpha j
alpha i < a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM2:(w.+1 != 0) * alpha i <= b ^ k
a * alpha j < a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
a * alpha j <= b ^ k ->
\sum_(i <= i1 < i + u.+1) alpha i1 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i1 < k + w.+1) b ^ i1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
a * alpha j <= b ^ k ->
\sum_(i <= i1 < i + u.+1) alpha i1 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i1 < k + w.+1) b ^ i1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaEb:a * alpha j = b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaEb:a * alpha j = b ^ k
a %| b ^ k ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaEb:a * alpha j = b ^ k
gcdn a (b ^ k) = a ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaEb:a * alpha j = b ^ k
1 = a ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j + \sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j +
(\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j.+1 <= i < j.+1 + v) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
(v != 0) * alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
(w.+1 != 0) * alpha i.+1 <= b ^ k
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
v1:nat
(v1.+1 != 0) * alpha i.+1 <= a * alpha j.+1
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
(w.+1 != 0) * alpha i.+1 <= b ^ k
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
(w.+1 != 0) * alpha i.+1 <= b ^ k
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
aM1:alpha i <= a * alpha j
aM2:alpha i <= b ^ k
alpha i.+1 <= b ^ k
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u, v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM3:alpha i.+1 <= a * alpha j.+1
aaLb:a * alpha j < b ^ k
aM1:alpha i <= a * alpha j
aM2:alpha i <= b ^ k
alpha i < b ^ k
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
(b ^ k + \sum_(k.+1 <= i < k + w.+1) b ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
b ^ k +
(\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i)
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
bL1:1 < b
n, u:nat
IH:forallvwnn0n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
aM3:alpha i.+1 <= a * alpha j.+1
bLaa:b ^ k < a * alpha j
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k.+1 <= i < k.+1 + w) b ^ i